es:ES, ff:FIFO, f2f+:F2F+-decls, sndr, rcvr:ff.C, e, e':E.
plus-ify{i:l}(es;ff;is_req  ;is_ack ;awaiting ;owes_ack )
 (f2f+-pred(e,e')  (f2f+-p+!(e,e'))) 

latex

Definitions	x:A. B(x), P  Q, P & Q, t  T, A c B, , f2f+-p+, A, False
Lemmas	f2f+-property, plus-ify wf, es-E wf, fifoC wf, F2F+-decls wf, FIFO wf, event system wf, rel-is-immediate, f2f+-pred wf, rel plus wf, f2f+-p+-sub-causl, es-causl transitivity2, es-causle weakening, es-causl irreflexivity, f2f+-pred-no-forks